GitHub - digamma-ai/CVE-2020-8835-verification: Formal verification example for CVE-2020-8835

Formal vefication of CVE-2021-31440

Set up environment

Install Linux headers: sudo apt install linux-headers-$(uname -r)
Install coq-config: pip install coq-config
Install OPAM: apt-get install opam
Initialize switch: coq-config
Switch to the new OPAM switch: opam switch ebpf_bug (you may need to re-open your shell after that)

Name		Name	Last commit message	Last commit date
Latest commit History 9 Commits
.gitignore		.gitignore
Makefile		Makefile
README.md		README.md
_CoqProject		_CoqProject
common.v		common.v
coq_config.yaml		coq_config.yaml
demo.c		demo.c
ebpf_bug.c		ebpf_bug.c
ebpf_fix.c		ebpf_fix.c
ebpf_proof.v		ebpf_proof.v
ebpf_proof_bug.v		ebpf_proof_bug.v